Termination Proof Script

Consider the TRS R consisting of the rewrite rule


1:	(((C : x) : y) : z) : u	→ (x : z) : (((x : y) : z) : u)

There are 5 dependency pairs:


2:	(((C : x) : y) : z) :# u	→ (x : z) :# (((x : y) : z) : u)
3:	(((C : x) : y) : z) :# u	→ x :# z
4:	(((C : x) : y) : z) :# u	→ ((x : y) : z) :# u
5:	(((C : x) : y) : z) :# u	→ (x : y) :# z
6:	(((C : x) : y) : z) :# u	→ x :# y

Consider the SCC {2-6}. By taking the AF π with π(:#) = 1 together with the lexicographic path order with empty precedence, the rules in {1-6} are strictly decreasing. Hence the TRS is terminating.

Tyrolean Termination Tool (0.05 seconds) --- May 3, 2006